ds:x:Id fp Type, da:k:Knd fp Type, A, B:ecl-trans-tuple{i:l}(ds;da),
f:((+Unit)()()), g:().
ecl-trans-normal(A)
 ecl-trans-normal(B)
 (m:. f(inr(),n.false,n.false,m))
 ecl-trans-normal(combine-ecl-tuples2(A;B;f;g)) 

latex

Definitions	t  T, x:A. B(x), b, P  Q, False, A, AB, , P  Q, P & Q, P  Q, Prop, , , True, T, Unit, finite-type(T), x. t(x), , no_repeats(T;l), sorted(L), Dec(P), let a,b,c,d,e,f,g = u in v(a;b;c;d;e;f;g), ecl-trans-normal(x), combine-ecl-tuples2(A;B;f;g), ecl-trans-tuple{i:l}(ds;da), Id, a:A fp B(a), Knd, false
Lemmas	bfalse wf, ecl-trans-normal wf, ecl-trans-tuple wf, Knd wf, fpf wf, Id wf, decidable equal product, decidable equal union, decidable equal bool, decidable equal unit, no repeats-merge, sorted-merge, nat plus wf, finite-type-product, finite-type-union, unit wf, finite-type-unit, finite-type-bool, not wf, assert wf, squash wf, true wf, it wf, bool wf, nat wf, eqff to assert, assert of bnot